i:Id, d:({k:Knd| hasloc(k;i)}  List).
{k:Knd| (k  d)}  r {k:{k:Knd| hasloc(k;i)} | (k  d)}  

latex

Definitions	False, P  Q, A, {T}, x:A. B(x), SQType(T), s = t, , ||as||, s ~ t, A  B, , , left + right, x:AB(x), T, True, P  Q, Dec(P), #$n, a < b, Void, x:A  B(x), A c B, x:A. B(x), (x  l), case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , b, xL. P(x), x. t(x), type List, Id, l[i], hasloc(k;i), b, Knd, {x:A| B(x)} , t  T
Lemmas	l member set, select wf, decidable assert, hasloc wf, Knd sq